Skip to content

Fix treap map/list bugs, tighten Treapability rule, expand tests - #29

Merged
ericeil merged 12 commits into
Certora:mainfrom
ericeil:main
Oct 30, 2026
Merged

ericeil merged 12 commits into
Certora:mainfrom
ericeil:main

Conversation

@ericeil

@ericeil ericeil commented Oct 30, 2026

Copy link
Copy Markdown
Collaborator

This PR fixes several bugs found while expanding test coverage, tightens the Treapability detekt rule, and makes the TreapList tests reproducible.

PR numbers in the commit titles (e.g. "(#3)") are pull requests on the fork ericeil/certora-collections, not on this repo.

Bug fixes

  • Hash-treap union merge with a stored null. HashTreapMap's shallow merger called shallowGetValue to decide whether a key was missing from the left side. That function returns null both for a missing key and for a stored null, so a key stored with a null value was merged twice. It now checks shallowContainsKey.
  • union/intersect with a plain Map threw NullPointerException (this[k]!!) when a key that both maps share had a null value on the treap side.
  • Parallel merge/union/intersect with parallelThresholdLog2 = 0 threw IllegalArgumentException, because the threshold minus one was passed as a negative log. A threshold of 0 is now accepted.
  • TreapListBuilder.size was captured when the builder was created and never updated.
  • TreapListBuilder list iterator:
    • set() replaced the builder's list but kept iterating the old one, so the iterator didn't see its own write.
    • add() and remove() didn't clear the last-returned position, so a following set() or remove() changed the wrong element instead of throwing IllegalStateException.

Treapability detekt rule

  • A hashCode() body that uses a property outside of any call (e.g. hashCode(): Int = b) or passes it to another function (e.g. Objects.hash(e)) is now checked. Before, it was skipped.
  • A property passed to TreapableHashCode.plus is exempt whether written it + e, it.plus(e), or it + (e).
  • The suggested fix for objects now names treapHashObject instead of the old utils.treapHashObject.

Tests

  • Many new tests for map, set, list, fork/join and TreapableHashCode operations, with shared helpers for map and set tests that were repeated.
  • TreapList node priorities can now be seeded per thread through an internal hook (TreapListNode.setTreapListPriorityRandom). A JUnit rule, TreapListPriorityRule, seeds it for each test, so TreapList shapes and coverage are the same on every run. Production code still uses Random.Default.

Testing

./gradlew test passes.

🤖 Generated with Claude Code

cursoragent and others added 12 commits October 29, 2026 21:18
The existing suite left merge, update, parallel bulk ops, set algebra, list
builders, and much of the treapability rule unexercised. These tests raise
JaCoCo line coverage of com.certora.collect from 60.5% to 91.2%. Product
bugs are pinned with ignored tests so the suite stays green. Copy-constructor
and negative-query tests were comparing the wrong collections.

Proved with the Gradle test tasks and a JaCoCo run. HashTreapMap mutation
testing killed all 80 covered mutants.

Co-authored-by: Eric Eilebrecht <ericeil@users.noreply.github.com>
Raise test coverage and record known collection bugs
getShallowMerger treated a null value as a missing key, so a key present with a null value was merged twice and could be stored twice in the bucket.

Co-authored-by: Eric Eilebrecht <ericeil@users.noreply.github.com>
The null-key, hash-key, copy-constructor, and iterator-removal cases were the same assertions with different arguments. Each scenario still runs, through one helper instead of a copied method.

Co-authored-by: Cursor Agent <cursoragent@cursor.com>
Co-authored-by: Eric Eilebrecht <ericeil@users.noreply.github.com>
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: ericeil <7407587+ericeil@users.noreply.github.com>
The size was copied once in the constructor, so add and clear left it stale while isEmpty read the updated list.

Co-authored-by: Cursor Agent <cursoragent@cursor.com>
Co-authored-by: Eric Eilebrecht <ericeil@users.noreply.github.com>
A hashCode body that returns a property directly was skipped because the reference has no parent call. Object diagnostics also named a utils.treapHashObject helper that does not exist.

Co-authored-by: Cursor Agent <cursoragent@cursor.com>
Co-authored-by: Eric Eilebrecht <ericeil@users.noreply.github.com>
set replaced the element in the builder but left the iterator on the previous treap, so previous still returned the old value.

Co-authored-by: Cursor Agent <cursoragent@cursor.com>
Co-authored-by: Eric Eilebrecht <ericeil@users.noreply.github.com>
fallbackUnion and fallbackIntersect forced the stored value with !!, so a null value threw NullPointerException before the merger ran.

Co-authored-by: Cursor Agent <cursoragent@cursor.com>
Co-authored-by: Eric Eilebrecht <ericeil@users.noreply.github.com>
parallelMerge, parallelUnion, and parallelIntersect subtracted one before the size check, so a threshold of 0 asked for a negative log and threw.

Co-authored-by: Cursor Agent <cursoragent@cursor.com>
Co-authored-by: Eric Eilebrecht <ericeil@users.noreply.github.com>
* Seed TreapList priorities so test coverage is reproducible

Node priorities came from Random.Default, so each JVM run built a different
tree and JaCoCo instruction coverage for getNodeAt and computeHashCode moved
between runs. Tests now install a seeded generator, with one fixed tree for
the branches a single random shape can miss. Production still uses
Random.Default when the override is null.

Co-authored-by: Eric Eilebrecht <ericeil@users.noreply.github.com>

* Keep TreapList priority seeds on the test thread

The shared Random required tests in one JVM not to overlap, and ProductBugTest
still built lists from Random.Default. Each test method that builds a TreapList
now gets its own seeded generator on the thread that runs it.

Co-authored-by: Eric Eilebrecht <ericeil@users.noreply.github.com>

---------

Co-authored-by: Cursor Agent <cursoragent@cursor.com>
Co-authored-by: Eric Eilebrecht <ericeil@users.noreply.github.com>
…layout (#10)

* Reset TreapListBuilder iterator state after add and remove.

The builder's list iterator kept lastReturnedIndex after add() and
remove(), so a following set() or remove() acted on whichever element
had shifted into that index instead of throwing IllegalStateException
as the ListIterator contract requires.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

* Exempt explicit and parenthesized TreapableHashCode.plus arguments.

The Treapability hashCode check exempted a property only when its
direct parent resolved to TreapableHashCode.plus. That covered
`it + e` but not `it.plus(e)` (the parent is a value argument) or
`it + (e)` (the parent is a parenthesized expression), so both were
reported. Look through parentheses and from a value argument to its
call before resolving.

Also fix a stale 'utils.HashCode.plus' reference in the rule's comment.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

* Describe the code, not the change, in recent comments.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

* Move ProductBugTest cases next to the behavior they cover.

The map cases now live in TreapMapTest, so they run against both the
hashed and sorted implementations (the null-value collision case stays
in HashTreapMapTest). The parallel zero-threshold case uses the same
larger maps as the existing parallel test. The list builder cases move
to TreapListTest.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>

---------

Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
@ericeil
ericeil merged commit 0fbf976 into Certora:main Oct 30, 2026
1 check passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants